T:Type, dT:EqDecider(T), L:(T List), x, y:T.
(x  L)  (y  L)  (index(L;x)  index(L;y))  (x before y  L  (x = y)) 

latex

Definitions	x:A. B(x), P  Q, P  Q, t  T, , {T}, T, P & Q, True, P  Q, P  Q, Dec(P), {i..j}
Lemmas	decidable lt, l index wf, int seg wf, length wf1, l before wf, le wf, l member wf, deq wf, l before l index, select wf, squash wf, non neg length, select l index